ds:x:Id fp Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da), n:, L:event-info(ds;da) List,
k:Knd, s:State(ds), v:Valtype(da;k).
ecl-trans-act(ds;da;A)(n,L @ [<k,s,v>])

(k  ecl-trans-ks(A)) & ecl-trans-a(A)(n,k,s,v,ecl-trans-state(A;L)) 

latex

Definitions

t  T, Valtype(da;k), P  Q, False, A, AB, , x:A. B(x), ecl-trans-state(v;L), ecl-trans-ks(v), Knd, (x  l), ecl-trans-a(v), b, A & B, event-info(ds;da), let x,y,z = a in t(x;y;z), Top, f(x)?z, KindDeq, x. t(x), State(ds), S  T, as @ bs, P & Q, x:A. B(x), ecl-trans-act(ds;da;A), {T}, SQType(T), Prop, True, T, Id, a:A fp B(a), ecl-trans-tuple{i:l}(ds;da), ecl-trans-type(A), , 1of(t), 2of(t), P  Q, ||as||, P  Q, P  Q

Lemmas

ecl-trans-act wf, ma-valtype wf, nat wf, general-append-cancellation, length wf1, cons one one, pi2 wf, pi1 wf, bool wf, squash wf, true wf, ecl-trans-tuple wf, fpf wf, Id wf, Knd sq, append wf, event-info wf, decl-state wf, fpf-cap wf, Kind-deq wf, top wf, assert wf, ecl-trans-a wf, l member wf, Knd wf, ecl-trans-ks wf, ecl-trans-state wf